/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package simhya.modelchecking.mtl;
import java.util.ArrayList;
import simhya.matheval.Expression;
import simhya.matheval.SymbolArray;
import simhya.model.store.Store;
import java.util.HashMap;

/**
 *
 * @author Luca
 */
public class MTLatom  extends MTLnode {
    String predicateString;
    Expression predicate;
    boolean constraint;

    public MTLatom(String predicateString, boolean constraint) {
        this.predicateString = predicateString;
        this.predicate = null;
        this.constraint = constraint;
    }
    
    @Override
    public void initalize(Store store, SymbolArray localSymbols, HashMap predicatesToExpression) {
        if (this.constraint) {
            predicate = store.parseExpression(predicateString, localSymbols);
            predicate.setLocalSymbols(localSymbols);
        } else {
            predicate = (Expression)predicatesToExpression.get(predicateString);
            if (predicate == null)
                throw new RuntimeException("Atomic predicate " + predicateString + " undefined");
        }  
    }
    
    @Override
     public String toFormulaTree(int depth) {
        String s = "";
        for (int i=0;i<depth;i++)
            s += "   ";
        s += this.predicateString + "\n";
        return s;
    }

    @Override
    ParametricInterval setExplorableTopNodes(String parameter) {
        if (this.isTopNode) {
            ParametricInterval I = new ParametricInterval();
            I.setUndefined();
            return I;
        } else return null;
    }

    @Override
    void labelingFormulaPointwiseSemantics(double[] deltaTimes) {
        //labelling has already been done for atoms
        return;
    }

    @Override
    void labelingTopFormulaPointwiseSemantics(double[] deltaTimes, boolean varyInterval, boolean varyRightBound, int points) {
        //labelling has already been done for atoms
        return;
    }

    @Override
    void collectAtomicNodes(ArrayList<MTLatom> list) {
        list.add(this);
    }
    
    void computeTruthValue(int i) {
        double x = this.predicate.computeValue();
        if (x == 1.0)
            this.truthValue[i] = true;
        else this.truthValue[i] = false;
    }
    
    
    
}
